Writing properties for hardware functionality verification in computer aided design is a difficult task. This is one of the main obstacles in applying formal verification techniques. Writing properties is difficult because hardware designers tend to write them in terms of implementations, whereas they should be specified at a higher functional level. This difficulty in functional verification reduces the advantages of computer aid design.